$\forall$$P$:$\mathbb{P}$, $d$:Dec($P$), $T$:Type, $A$:($P$$\rightarrow$$T$), $B$:$T$. if $p$:$P$ then $A$($p$) else $B$ fi  $\in$ $T$